#include <iostream>
#include "PDTGraphClone.h"
#include "PDTCodeGraph.h"

#include "PDTAssign.h"
#include "PDTNumVar.h"
#include "PDTVar.h"
#include "PDTExpBoolBinNumDerived.h"
#include "PDTExpNumBinDerived.h"
#include "PDTProp.h"
#include "PDTNumConst.h"
#include "PDTBoolVar.h"
#include "PDTExpBoolBinBoolDerived.h"
#include "PDTSetOp.h"
#include "PDTIfElse.h"
#include "PDTAssert.h"
#include "PDTListOfStatements.h"
#include "PDTType.h"
#include "PDTSetVar.h"
#include "PDTQuantifier.h"
#include "PDTBoolConst.h"
#include "PDTNeg.h"
#include "PDTNot.h"
#include "PDTWhile.h"
#include "PDTFunction.h"


PDTGraphCloneTraversal::PDTGraphCloneTraversal(PDTCodeGraph & aOcg, PDTCodeGraph & aRcg, PDTNode * aTopNode):
    PDTLinearTraversalIfc(aOcg),
    rcg(aRcg),
    topNode(aTopNode),
    pendingPre(NULL),
    isFirstPre(true),
    preCount(0),
    size(aOcg.nodes.size()) {
        // set up the clones map 
        clones = new PDTNode * [size];
        for (unsigned int i = 0; i < size; i++) 
            clones[i] = NULL;

        if (fixVariables() == Stop) {
            // TODO: throw exception
        }

        if (traverse() == Stop) {
            //TODO: exception
        }
    }

Traversal::RetType
PDTGraphCloneTraversal::fixVariables() {
    /* Initializing all sequences */
    for (unsigned int i = 0; i < ocg.nodes.size(); i++) {
        PDTNode * node = ocg.nodes[i];
        if (node->isSequence()) {
            if (node->traverseEx(*this) == Stop) {
                olog() << "Received Stop signal" << endl;
                stringstream ss;
                node->toString(ss);
                cout << ss.str() << endl;
                return Stop;
            }
        } 
    }

    typedef map < int, bool* > SeqId2Assigned_t;
    typedef queue<PDTNode*> SequenceVarQueue_t;
    SeqId2Assigned_t seqId2Assigned;
    SequenceVarQueue_t sequenceVarQueue;
    /* Initialize all variables and then check is any needs PI assignments */
    for (unsigned int i = 0; i < ocg.variables.size(); i++) {
        PDTVar * var = ocg.variables[i];
        PDTNode * node = var->getNode();
        if (node->traverseEx(*this) == Stop) {
            olog() << "Received Stop Signal" << endl;
            return Stop;
        } 

        if (node->isSequenceVar()) {
            sequenceVarQueue.push(node);
            continue;
        }
        
        vector <PDTNode*> & parents = node->getParents();
        if (parents.size() == 0) {
            olog() << "Unused variable" << endl;
            continue;
        }

        if (node->isSequenceAccessNum() ) {
            PDTSequenceAccessNum * access = dynamic_cast<PDTSequenceAccessNum *>(node);
            assert(access != NULL); // assertion to make sure nothing goes wrong in dynamic_cast<>
            PDTExpNum * exp = access->getRight();
            PDTNode * nExp = (PDTNode*)exp;
            if (!nExp->isNumConstInt()) {
                continue;
            } else {
                // set this sequence access num as visited 
                PDTSequenceVar * seqVar = access->getLeftVar();
                assert(seqVar != NULL); // assertion to make sure nothing went wrong when casting
                unsigned int id = seqVar->getId();
                unsigned int seqSize = seqVar->getSequence()->getSize();
                if (seqId2Assigned[id] == NULL) {
                    seqId2Assigned[id] = new bool[seqSize];
                }

                PDTNumConstInt * index = dynamic_cast<PDTNumConstInt*>(nExp);
                assert(index != NULL); // safeguarding conditions
                int val = index->getValue();
                (seqId2Assigned[id])[val] = true;
            }
        }

        bool remove = false; // any need to remove from the graph
        bool needsPi = isUsedBefore(*var, remove); // any need to assign primary inputs

        if (remove) {
            // TODO: need to remove this node from the graph
            olog() << "Assignment needs to be removed" << endl;
        }

        if (needsPi){
            // used before first assign => needs pi
            // create a pi assignment in new graph
            PDTNode * cNode = getClone(node);
            if (cNode == NULL) {
                olog() << "graph cloning failed: program will now exit" << endl;
                exit(EXIT_FAILURE);
            }

            PDTVar * cVar = dynamic_cast<PDTVar*>(cNode);
            if (cVar == NULL) {
                olog() << "graph cloning failed: program will now exit" << endl;
                exit(EXIT_FAILURE);
            }

            if (cNode->isSequenceAccessNum()) {
                PDTSequenceAccessNum * cloned = dynamic_cast<PDTSequenceAccessNum*>(cNode);
                PDTSequenceVar * lVar = cloned->getLeftVar();
                PDTExpNum * lexp = cloned->getRight();
                PDTSequenceAccessNum * nVar = new PDTSequenceAccessNum(rcg, *lVar, *lexp);
                cVar = nVar;
            }

            PDTPiAssign * piAssign = new PDTPiAssign(rcg, *cVar);
            if (piAssign == NULL) {
                olog() << "graph cloning failed: program will now exit" << endl;
                exit(EXIT_FAILURE);
            }
        }
    }

    /* 
     * Go over the sequence variables and check in each 
     * for the elements. If they are not visited before, i.e.
     * not already initialized or checked before then should 
     * inilialize them to primary inputs.
    */
    typedef map<int, PDTNumConstInt*> Int2Const_t;
    Int2Const_t int2Const;
    while(!sequenceVarQueue.empty()) {
        PDTSequenceVar * seqVar = dynamic_cast<PDTSequenceVar*>(sequenceVarQueue.front());
        assert(seqVar != NULL); //safeguarding
        if (seqVar == NULL) {
            olog() << "sequence queue is corrupt" << endl;
            exit(EXIT_FAILURE);
        }
        sequenceVarQueue.pop();

        unsigned int seqSize = seqVar->getSequence()->getSize();
        unsigned int seqId = seqVar->getId();
        if (seqId2Assigned[seqId] == NULL) {
            for (unsigned int i = 0; i < seqSize; i++) {
                PDTNumConstInt * cnst;
                if (int2Const[i] == NULL) {
                    cnst = new PDTNumConstInt(rcg, i);
                    int2Const[i] = cnst;
                } else {
                    cnst = int2Const[i];
                }

                PDTSequenceAccessNum * new_access = new PDTSequenceAccessNum(rcg, *seqVar, *cnst);
                PDTPiAssign * piAssign = new PDTPiAssign(rcg, *new_access);
                if (piAssign == NULL) {
                    olog() << "graph cloning failed: program will now exit" << endl;
                    exit(EXIT_FAILURE);
                }
            }
        } else {
            bool * & isVisited = seqId2Assigned[seqId];
            for (unsigned int i = 0; i < seqSize; i++) {
                if (isVisited[i])
                    continue;

                PDTNumConstInt * cnst;
                if (int2Const[i] == NULL) {
                    cnst = new PDTNumConstInt(rcg, i);
                    int2Const[i] = cnst;
                } else {
                    cnst = int2Const[i];
                }

                PDTSequenceAccessNum * new_access = new PDTSequenceAccessNum(rcg, *seqVar, *cnst);
                PDTPiAssign * piAssign = new PDTPiAssign(rcg, *new_access);
                if (piAssign == NULL) {
                    olog() << "graph cloning failed: program will now exit" << endl;
                    exit(EXIT_FAILURE);
                }
            }
        }
    }

    return Continue;
}

PDTGraphCloneTraversal::~PDTGraphCloneTraversal() {
    delete [] clones;
}

PDTNode * 
PDTGraphCloneTraversal::getChildClone(PDTNode & d, unsigned int childNum) const {
    vector<PDTNode * > & children = d.getChildren();
    PDTNode * child = children[childNum];
    PDTNode * clone = getClone(child);
    return clone;
}

bool 
PDTGraphCloneTraversal::setClone(PDTNode & d, PDTNode * clone) {
    unsigned int id = d.getId();
    clones[id] = clone;
    return true;
}

bool 
PDTGraphCloneTraversal::setVarClone(PDTVar & d, PDTVar * clone) {
    PDTNode * dNode = d.getNode();
    PDTNode * dClone = clone->getNode();
    unsigned int id = dNode->getId();
    clones[id] = dClone;
    return true;
}

PDTNode * 
PDTGraphCloneTraversal::getClone(PDTNode & d) const {
    unsigned int id = d.getId();
    return clones[id];
}

PDTNode * 
PDTGraphCloneTraversal::getClone(PDTNode * d) const {
    unsigned int id = d->getId();
    return clones[id];
}
    
bool 
PDTGraphCloneTraversal::isTopNode(PDTNode * node) const {
    return node == topNode;
}


#define CLONE_BINARY_OP_LR(CLS_NAME, LEFT_OP_TYPE, RIGHT_OP_TYPE) \
    if (getClone(d) != NULL) \
        return Traversal::Continue; \
    LEFT_OP_TYPE * lft = dynamic_cast<LEFT_OP_TYPE*>(getChildClone(d, 0)); \
    if (lft == NULL)  { \
        stringstream ss; \
        d.toString(ss); \
        cout << ss.str() << endl; \
        olog() << "left child is NULL" << endl; \
        return Traversal::Stop; \
    }\
    RIGHT_OP_TYPE * rgt = dynamic_cast<RIGHT_OP_TYPE*> (getChildClone(d, 1)); \
    if (rgt == NULL) { \
        stringstream ss; \
        d.toString(ss); \
        cout << ss.str() << endl; \
        olog() << "right child is NULL" << endl; \
        return Traversal::Stop; \
    }\
    PDTNode * clone = new CLS_NAME(rcg, *lft, *rgt); \
    if (clone == NULL) {\
        olog() << "Sending Stop flag" << endl; \
        return Traversal::Stop; \
    }\
    setClone(d,clone); \
    return  Traversal::Continue;


#define CLONE_BINARY_OP(CLS_NAME, OPERAND_TYPE) \
        CLONE_BINARY_OP_LR(CLS_NAME, OPERAND_TYPE, OPERAND_TYPE)


#define CLONE_UNARY_OP(CLS_NAME, OP_TYPE) \
    if (getClone(d) != NULL) \
        return Traversal::Continue; \
    PDTNode* cClone = getChildClone(d,0); \
    OP_TYPE* expClone = dynamic_cast<OP_TYPE*>(cClone); \
    if (expClone == NULL) \
        return Traversal::Stop; \
    CLS_NAME * clone = new CLS_NAME(rcg, *expClone); \
    if (clone == NULL) \
        return Traversal::Stop; \
    setClone(d,clone); \
    return Traversal::Continue;

#define CLONE_CONST() \
    if (getClone(d) != NULL) \
         setClone(d,&d); \
    return Traversal::Continue;

#define NOT_IMPLEMENTED_YET \
    olog() << "Not implemented yet!" << endl;

#define CLONE_VAR(CLS_NAME) \
    if (getClone(d) != NULL) \
        return Traversal::Continue; \
    PDTFunctionDec * funcDec = d.getFunctionDec(); \
    if (! isTopNode((PDTNode*)funcDec)) { \
        setClone(d,&d); \
        return Traversal::Continue; \
    } \
    const string & name = d.getName(); \
    if (d.getRange() != NULL) { \
        PDTIntRange * cloneRange = dynamic_cast<PDTIntRange*>(getClone(d.getRange())); \
        if (cloneRange == NULL) { \
            return Traversal::Stop; \
        }\
        CLS_NAME * clone = new CLS_NAME(rcg, name, NULL, cloneRange); \
        if (clone == NULL) \
            return Traversal::Stop; \
        setClone(*(d.getNode()),  clone->getNode()); \
        return Traversal::Continue; \
    }\
    CLS_NAME * clone = new CLS_NAME(rcg, name); \
    if(clone == NULL) \
        return Traversal::Stop; \
    setClone(*(d.getNode()), clone->getNode()); \
    return Traversal::Continue; 

#define CLONE_SEQ_VAR(CLS_NAME,Seq) \
    if (getClone(d) != NULL) \
        return Traversal::Continue; \
    PDTFunctionDec * funcDec = d.getFunctionDec(); \
    if (! isTopNode((PDTNode*)funcDec)) { \
        setClone(d,&d); \
        return Traversal::Continue; \
    } \
    const string & name = d.getName(); \
    CLS_NAME * clone = new CLS_NAME(rcg, *Seq, name); \
    if(clone == NULL) \
        return Traversal::Stop; \
    setClone(d,clone); \
    return Traversal::Continue;

#define CLONE_QUANTIFIER(Q_TYPE) \
    unsigned int i = 0; \
    vector <PDTVar *> vars; \
    for (; i < d.getNumVars(); i++) { \
        PDTNode * clone = getChildClone(d,i); \
        if (clone == NULL) \
            return Traversal::Stop; \
        PDTVar * vClone = dynamic_cast<PDTVar *>(clone); \
        vars.push_back(vClone); \
    } \
    PDTNode* nodeClone = getChildClone(d,i); \
    PDTExpBool * expClone = dynamic_cast<PDTExpBool*>(nodeClone); \
    if (expClone == NULL) \
        return Traversal::Stop; \
    Q_TYPE * clone = new Q_TYPE(rcg, vars, *expClone); \
    if (clone == NULL)  \
        return Traversal::Stop; \
    setClone(d,clone); \
    return Traversal::Continue;


// PDTAdd 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTAdd & d) {
    CLONE_BINARY_OP(PDTAdd,PDTExpNum)
}


// PDTAnd 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTAnd & d) {
    CLONE_BINARY_OP(PDTAnd,PDTExpBool)
}


// PDTAssert 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTAssert & d) {
    if (getClone(d) != NULL)
        return Traversal::Skip;

    PDTExpBool * exp = d.getExpression();
    if (exp == NULL) {
        olog() << "sending stop signal!" << endl;
        return Traversal::Stop;
    }
    PDTExpBool * expClone = dynamic_cast<PDTExpBool*>(getClone(exp));
    if (expClone == NULL) {
        olog() << "sending stop signal!" << endl;
        return Traversal::Stop;
    }

    PDTAssert * assertClone =  new PDTAssert(rcg, *expClone);
    setClone(d, assertClone);
    return Traversal::Continue;
}


// PDTAssign 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTAssign & d) {
    CLONE_BINARY_OP_LR(PDTAssign,PDTVar,PDTExp)
}


// PDTBehavior 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTBehavior & d) {
    NOT_IMPLEMENTED_YET
    return Traversal::Continue;
}


// PDTBehaviors 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTBehaviors & d) {
    NOT_IMPLEMENTED_YET
    return Traversal::Continue;
}


// PDTBoolConst 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTBoolConst & d) {
    if (getClone(d) != NULL)
        return Traversal::Continue;

    PDTBoolConst * cloneConst = new PDTBoolConst(rcg, d.getBoolean());
    if (cloneConst == NULL)
        return Traversal::Stop;

    setClone(d, cloneConst);
    return Traversal::Continue;
}


// PDTBoolVar 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTBoolVar & d) {
    if (getClone(d) != NULL) 
        return Traversal::Continue; 
    PDTFunctionDec * funcDec = d.getFunctionDec(); 
    if (! isTopNode((PDTNode*)funcDec)) { 
        setClone(d,&d); 
        return Traversal::Continue; 
    } 
    const string & name = d.getName(); 
    PDTBoolVar * clone = new PDTBoolVar(rcg, name); 
    if(clone == NULL) 
        return Traversal::Stop;
    setClone(*(d.getNode()), clone->getNode()); 
    return Traversal::Continue; 
}

// PDTConstSequence 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTConstSequence & d) {
    CLONE_CONST()
    return Traversal::Continue;
}


// PDTDiv 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTDiv & d) {
    CLONE_BINARY_OP(PDTDiv,PDTExpNum)
}


// PDTEqualBool 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTEqualBool & d) {
    CLONE_BINARY_OP(PDTEqualBool,PDTExpBool)
}


// PDTEqualNum 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTEqualNum & d) {
    CLONE_BINARY_OP(PDTEqualNum,PDTExpNum)
}


// PDTExist 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTExist & d) {
    if (getClone(d) != NULL)
	return Traversal::Continue;

    // get cloned vars vector
    unsigned int i = 0;
    vector <PDTVar *> vars;
    for (; i < d.getNumVars(); i++) {
	PDTNode * clone = getChildClone(d,i);
	if (clone == NULL) {
	    olog() << " sending Stop flag!" << endl;
	    return Traversal::Stop;
	}
	PDTVar * vClone = dynamic_cast<PDTVar*>(clone);
	vars.push_back(vClone);
    }

    // get cloned expression
    PDTNode * nodeClone = getChildClone(d,i);
    PDTExpBool * expClone = dynamic_cast<PDTExpBool*>(nodeClone);
    if (expClone == NULL) {
	olog() << " sending Stop flag!" << endl;
	return Traversal::Stop;
    }

    /**  -- translate it into the while loop --    
     *  res = false;
     *  while (var1 in range) 
     *   while (var2 in range)
     *    while (var3 in range)
     *      ....
     *       res = res || exp;
     */
    // set up return boolean variable
    string retname = "_ExistReturn_";
    ostringstream oss;
    oss << d.getId();
    retname += oss.str();
    PDTBoolVar * retVar = new PDTBoolVar(rcg, retname);
    PDTBoolConst * _true = new PDTBoolConst(rcg, false);
    PDTAssign * initalizeTrue = new PDTAssign(rcg, *retVar, *_true);

    unsigned int varSize = vars.size();
    vector <PDTExpBool*> whileExpressions;
    vector < vector<PDTStatement *> > whileStatements(varSize);
    PDTNumConstInt * one = new PDTNumConstInt(rcg, 1);
    PDTAssign * parentAssign;
    for (unsigned int j = 0; j < varSize; j++) {
        // create while loop condition for each variable
        PDTVar * var = vars[j];
        if (var->getNode()->isNumVar()) {
            unsigned int idx = (j > 0) ? j-1:j;
            vector < PDTStatement * > & varStmt = whileStatements[idx];
            PDTNumVar * numVar = dynamic_cast <PDTNumVar*> (var);
            PDTIntRange * varRange = numVar->getRange();

            PDTExp * start = varRange->getStart();
            PDTExp * end = varRange->getEnd();

            // numVar = start
            PDTAssign * initialize = new PDTAssign(rcg, *numVar, *start);
            if (j >= 1)
                varStmt.insert(varStmt.begin(),initialize);
            else if (j == 0)
                parentAssign = initialize;

            // numVar <= end
            PDTExpNum * op1 = (PDTExpNum*)numVar->getNode();
            PDTExpNum * op2 = (PDTExpNum*)end;
            PDTLessThanEqual * leq = new PDTLessThanEqual (rcg, *op1, *op2);
            whileExpressions.push_back(leq);

            // numVar = numVar + 1;
            PDTAdd * varPlusOne = new PDTAdd(rcg, *op1, *one);
            PDTAssign * varIncrement = new PDTAssign(rcg, *numVar, *varPlusOne);
            whileStatements[j].push_back(varIncrement);

        } else if (var->getNode()->isSetVar()) {
            //TODO: to be updated
        }
    }

    // we have now the entire list of whileExpressions
    // set up inner while loop
    PDTExpBool * op1 = dynamic_cast<PDTExpBool*>(retVar->getNode());
    PDTOr * stmtOr = new PDTOr(rcg, *op1, *expClone);
    PDTAssign * assignAnd = new PDTAssign(rcg, *retVar, *stmtOr);
    vector <PDTStatement *> & varStmt = whileStatements[varSize-1];
    varStmt.insert(varStmt.begin(), assignAnd);
    PDTListOfStatements * whileList = new PDTListOfStatements(rcg, varStmt);
    PDTExpBool * cond = whileExpressions[varSize-1];
    PDTWhile * innerWhile = new PDTWhile(rcg, *cond, *whileList);

    // set up the rest of while loops
    PDTWhile * prevWhile = innerWhile;
    for(int j = varSize - 2; j >= 0; j--) {
        vector < PDTStatement * > & varStmt = whileStatements[j];
        PDTExpBool * boolExp = whileExpressions[j];
        varStmt.insert(varStmt.end()-1, prevWhile);
        PDTListOfStatements * whileList = 
            new PDTListOfStatements(rcg, varStmt);
        PDTWhile * currWhile = new PDTWhile(rcg, *boolExp, *whileList);
        prevWhile = currWhile;
    }

    setClone(d, retVar->getNode()); 

    // Now save all in one List of Statements
    // initalizeTrue , parentAssign , prevWhile
    vector < PDTStatement * > statements;
    statements.push_back(initalizeTrue);
    statements.push_back(parentAssign);
    statements.push_back(prevWhile);
    PDTListOfStatements * list = new PDTListOfStatements(rcg, statements);
    quantifierStatement[d.getId()] = list;

    whileStatements.clear();
    whileExpressions.clear();
    statements.clear();
    return Traversal::Continue;
}


// PDTForall 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTForall & d) {
    //CLONE_QUANTIFIER(PDTForall)
    if (getClone(d) != NULL)
        return Traversal::Continue;

    // get cloned vars vector
    unsigned int i = 0; 
    vector <PDTVar *> vars; 
    for (; i < d.getNumVars(); i++) { 
        PDTNode * clone = getChildClone(d,i); 
        if (clone == NULL) 
            return Traversal::Stop; 
        PDTVar * vClone = dynamic_cast<PDTVar *>(clone); 
        vars.push_back(vClone); 
    } 

    // get cloned expression
    PDTNode* nodeClone = getChildClone(d,i); 
    PDTExpBool * expClone = dynamic_cast<PDTExpBool*>(nodeClone); 
    if (expClone == NULL) 
        return Traversal::Stop; 
    
    /**  -- translate it into the while loop --    
     *  res = true;
     *  while (var1 in range) 
     *   while (var2 in range)
     *    while (var3 in range)
     *      ....
     *       res = res & exp;
     */
    // set up return boolean variable
    string retname = "_ForAllReturn_";
    ostringstream oss;
    oss << d.getId();
    retname += oss.str();
    PDTBoolVar * retVar = new PDTBoolVar(rcg, retname);
    PDTBoolConst * _true = new PDTBoolConst(rcg, true);
    PDTAssign * initalizeTrue = new PDTAssign(rcg, *retVar, *_true);

    unsigned int varSize = vars.size();
    vector <PDTExpBool*> whileExpressions;
    vector < vector<PDTStatement *> > whileStatements(varSize);
    PDTNumConstInt * one = new PDTNumConstInt(rcg, 1);
    PDTAssign * parentAssign;
    for (unsigned int j = 0; j < varSize; j++) {
        // create while loop condition for each variable
        PDTVar * var = vars[j];
        if (var->getNode()->isNumVar()) {
            unsigned int idx = (j > 0) ? j-1:j;
            vector < PDTStatement * > & varStmt = whileStatements[idx];
            PDTNumVar * numVar = dynamic_cast <PDTNumVar*> (var);
            PDTIntRange * varRange = numVar->getRange();

            PDTExp * start = varRange->getStart();
            PDTExp * end = varRange->getEnd();

            // numVar = start
            PDTAssign * initialize = new PDTAssign(rcg, *numVar, *start);
            if (j >= 1)
                varStmt.insert(varStmt.begin(),initialize);
            else if (j == 0)
                parentAssign = initialize;

            // numVar <= end
            PDTExpNum * op1 = (PDTExpNum*)numVar->getNode();
            PDTExpNum * op2 = (PDTExpNum*)end;
            PDTLessThanEqual * leq = new PDTLessThanEqual (rcg, *op1, *op2);
            whileExpressions.push_back(leq);

            // numVar = numVar + 1;
            PDTAdd * varPlusOne = new PDTAdd(rcg, *op1, *one);
            PDTAssign * varIncrement = new PDTAssign(rcg, *numVar, *varPlusOne);
            whileStatements[j].push_back(varIncrement);

        } else if (var->getNode()->isSetVar()) {
            //TODO: to be updated
        }
    }

    // we have now the entire list of whileExpressions
    // set up inner while loop
    PDTExpBool * op1 = dynamic_cast<PDTExpBool*>(retVar->getNode());
    PDTAnd * stmtAnd = new PDTAnd(rcg, *op1, *expClone);
    PDTAssign * assignAnd = new PDTAssign(rcg, *retVar, *stmtAnd);
    vector <PDTStatement *> & varStmt = whileStatements[varSize-1];
    varStmt.insert(varStmt.begin(), assignAnd);
    PDTListOfStatements * whileList = new PDTListOfStatements(rcg, varStmt);
    PDTExpBool * cond = whileExpressions[varSize-1];
    PDTWhile * innerWhile = new PDTWhile(rcg, *cond, *whileList);

    // set up the rest of while loops
    PDTWhile * prevWhile = innerWhile;
    for(int j = varSize - 2; j >= 0; j--) {
        vector < PDTStatement * > & varStmt = whileStatements[j];
        PDTExpBool * boolExp = whileExpressions[j];
        varStmt.insert(varStmt.end()-1, prevWhile);
        PDTListOfStatements * whileList = 
            new PDTListOfStatements(rcg, varStmt);
        PDTWhile * currWhile = new PDTWhile(rcg, *boolExp, *whileList);
        prevWhile = currWhile;
    }

    setClone(d, retVar->getNode()); 

    // Now save all in one List of Statements
    // initalizeTrue , parentAssign , prevWhile
    vector < PDTStatement * > statements;
    statements.push_back(initalizeTrue);
    statements.push_back(parentAssign);
    statements.push_back(prevWhile);
    PDTListOfStatements * list = new PDTListOfStatements(rcg, statements);
    quantifierStatement[d.getId()] = list;

    whileStatements.clear();
    whileExpressions.clear();
    statements.clear();
    return Traversal::Continue;
}


// PDTFunctionCall 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTFunctionCall & d) {
    unsigned int i = 0; 
    vector <PDTNode *> args; 
    for (; i < d.getArgumentCount(); i++) {
        PDTNode * clone = getChildClone(d,i); 
        if (clone == NULL)
            return Traversal::Stop;
        args.push_back(clone); 
    } 
    //TODO: check what happens to the return var!

    PDTFunctionDec * funcPtr = d.getFuncPtr();
    PDTNode * funcClone = getClone(funcPtr);
    PDTFunctionDec * funcDecClone = dynamic_cast<PDTFunctionDec*>(funcClone);
    if (funcDecClone == NULL)
        return Traversal::Stop;

    string name = d.getName();
    PDTFunctionCall * clone = new PDTFunctionCall(rcg, args, name, funcDecClone);
    if (clone == NULL)
        return Traversal::Stop;
    setClone(d,clone);
    return Traversal::Continue;
}


// PDTFunctionDec 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTFunctionDec & d) {
    if (getClone(d) != NULL)
        return Traversal::Continue;

    unsigned int i = 0; 
    vector <PDTVar *> args; 
    for (; i < d.getArgumentCount(); i++) {
        PDTNode * clone = getChildClone(d,i); 
        PDTVar * vClone = dynamic_cast<PDTVar *>(clone);
        if (vClone == NULL)
            return Traversal::Stop;
        args.push_back(vClone);
    } 
    PDTVar * retVar  = d.getReturnVar();
    PDTNode * retNode = retVar->getNode();
    PDTNode * retClone = getClone(*retNode);
    PDTVar * retVarClone = dynamic_cast<PDTVar*>(retClone);
    if (retVarClone == NULL)
        return Traversal::Stop;

    PDTListOfStatements* list = d.getStatements();
    PDTNode * listNodeClone = getClone(*list);
    PDTListOfStatements* listClone = dynamic_cast<PDTListOfStatements*>(listNodeClone);
    if (listClone == NULL) 
        return Traversal::Stop;

    string name = d.getName();

    PDTFunctionDec * clone = new PDTFunctionDec(rcg, name,*listClone, retVarClone, args);

    if (clone == NULL)
        return Traversal::Stop;
    setClone(d,clone);
    return Traversal::Continue;
}

// PDTGreaterThan 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTGreaterThan & d) {
    CLONE_BINARY_OP(PDTGreaterThan,PDTExpNum)
}


// PDTGreaterThanEqual 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTGreaterThanEqual & d) {
    CLONE_BINARY_OP(PDTGreaterThanEqual,PDTExpNum)
}


// PDTIfElse 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTIfElse & d) {
    PDTNode * temp = getClone(d);
    if (temp != NULL)
        return Traversal::Continue;
    PDTExpBool* cond = d.getCondition();
    PDTExpBool* condClone = dynamic_cast<PDTExpBool*>(getClone(cond));
    if (condClone == NULL)
        return Traversal::Stop;

    PDTStatement* ifStatement = d.getIfResult();
    PDTNode * cloneNode;
    int childid;
    if (ifStatement->isQuantifier()) 
        cloneNode = quantifierStatement[ifStatement->getId()];
    else if ((childid = hasQuantifier(ifStatement)) != -1)
        cloneNode = quantifierHandler(ifStatement, childid);
    else 
        cloneNode = getClone(*ifStatement);
    PDTStatement* ifClone = dynamic_cast<PDTStatement*>(cloneNode);
    if (ifClone == NULL)
        return Traversal::Stop;

    PDTStatement* elseStatement = d.getElseResult();
    PDTNode * nodeClone;
    if (elseStatement->isQuantifier())
        nodeClone = quantifierStatement[elseStatement->getId()];
    else if ((childid = hasQuantifier(elseStatement)) != -1)
        nodeClone = quantifierHandler(elseStatement, childid);
    else 
        nodeClone = getClone(*elseStatement);
    PDTStatement* elseClone = dynamic_cast<PDTStatement*>(nodeClone);
    if (elseClone == NULL)
        return Traversal::Stop;

    PDTIfElse * clone = new PDTIfElse(rcg, *condClone, *ifClone, *elseClone);
    if (clone == NULL) 
        return Traversal::Stop;
    setClone(d,clone);
    return Traversal::Continue;
}


// PDTImplies 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTImplies & d) {
    if (getClone(d) != NULL)
	return Traversal::Continue;

    PDTExpBool * left = d.getLeft();
    PDTExpBool * right = d.getRight();

    PDTNode * lNode = getClone(left);
    PDTNode * rNode = getClone(right);
    if (lNode == NULL || rNode == NULL) {
	olog() << "sending Stop flag" << endl;
	return Traversal::Stop;
    }

    PDTExpBool * lClone = dynamic_cast<PDTExpBool*>(lNode);
    PDTExpBool * rClone = dynamic_cast<PDTExpBool*>(rNode);
    if (lClone == NULL || rClone == NULL) {
	olog() << "sending Stop flag" << endl;
	return Traversal::Stop;
    }

    PDTImplies * clone = new PDTImplies(rcg, *lClone, *rClone);
    if (clone == NULL) {
	olog() << "sending Stop flag" << endl;
	return Traversal::Stop;
    }

    setClone(d, clone);
    return Traversal::Continue;
}


// PDTIntRange 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTIntRange & d) {
    if (getClone(d) != NULL)
        return Traversal::Continue;


    PDTExp * start = d.getStart();
    PDTExp * end = d.getEnd();

    PDTExp * startClone = dynamic_cast<PDTExp*>(getClone(start));
    if (startClone == NULL) return Traversal::Stop;
    PDTExp * endClone = dynamic_cast<PDTExp*>(getClone(end));
    if (endClone == NULL) return Traversal::Stop;

    PDTIntRange * clone = new PDTIntRange(rcg, "cloneRange", startClone, endClone);

    setClone(d, clone);
    return Traversal::Continue;
}


// PDTInvariant 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTInvariant & d) {
    NOT_IMPLEMENTED_YET
    return Traversal::Continue;
}


// PDTLessThan 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTLessThan & d) {
    cout << "Less Than" << endl;
    stringstream ss;
    d.toString(ss);
    cout << ss.str();
    cout << "=======" << endl;
    CLONE_BINARY_OP(PDTLessThan,PDTExpNum)
}


// PDTLessThanEqual 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTLessThanEqual & d) {
    CLONE_BINARY_OP(PDTLessThanEqual,PDTExpNum)
}


// PDTListOfStatements 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTListOfStatements & d) {
    vector<PDTStatement*> statements;
    for (unsigned int i=0; i<d.numberOfStmts(); i++){
        PDTNode & child = d.getChildEx(i);
        PDTNode * clone;
        int childid;
        if (child.isQuantifier())
            clone = quantifierStatement[child.getId()];
        else if ((childid = hasQuantifier(&child)) != -1)
            clone = quantifierHandler(&child, childid);
        else
            clone = getChildClone(d,i);
        PDTStatement * statement = dynamic_cast<PDTStatement*>(clone);
        if (statement == NULL)
            return Traversal::Stop;
        statements.push_back(statement);
    }
    PDTListOfStatements * clone = new PDTListOfStatements(rcg, statements);
    if (clone == NULL)
        return Traversal::Stop;
    setClone(d,clone);
    return Traversal::Continue;
}

// PDTMod 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTMod & d) {
    CLONE_BINARY_OP(PDTMod,PDTExpNum)
}


// PDTMult 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTMult & d) {
    CLONE_BINARY_OP(PDTMult,PDTExpNum)
}

// PDTNeg 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTNeg & d) {
    CLONE_UNARY_OP(PDTNeg, PDTExpNum) 
}


// PDTNilStatement 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTNilStatement & d) {
    if(getClone(d) == NULL)
        setClone(d,&d);
    return Traversal::Continue;
}


// PDTNot 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTNot & d) {
    CLONE_UNARY_OP(PDTNot, PDTExpBool) 
}


// PDTNotEqualBool 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTNotEqualBool & d) {
    CLONE_BINARY_OP(PDTNotEqualBool,PDTExpBool)
}


// PDTNotEqualNum 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTNotEqualNum & d) {
    CLONE_BINARY_OP(PDTNotEqualNum,PDTExpNum)
}


// PDTNumConst 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTNumConst & d) {
    CLONE_CONST()
}


// PDTNumConstDbl 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTNumConstDbl & d) {
    CLONE_CONST()
}


// PDTNumConstInt 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTNumConstInt & d) {
    if (getClone(d) != NULL)
        return Traversal::Continue;

    PDTNumConstInt * cloneConst = new PDTNumConstInt(rcg, d.getValue());
    if (cloneConst == NULL) {
        olog() << "sending stop signal!" << endl;
        return Traversal::Stop;
    }

    setClone(d, cloneConst);
    return Traversal::Continue;
}


// PDTNumVar 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTNumVar & d) {
    CLONE_VAR(PDTNumVar)
}


// PDTOr 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTOr & d) {
    CLONE_BINARY_OP(PDTOr,PDTExpBool)
}


// PDTPair 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTPair & d) {
    NOT_IMPLEMENTED_YET
    return Traversal::Continue;
}


// PDTPostCondition 
Traversal::RetType PDTGraphCloneTraversal :: pre(PDTPostCondition & d) {
    cout << "IN PDTPostCondition pre" << endl;
    return Traversal::Continue;
}

Traversal::RetType PDTGraphCloneTraversal :: post(PDTPostCondition & d) {
    if (getClone(d) != NULL)
	return Traversal::Skip;

    PDTExpBool * exp = d.getExpression();
    if (exp == NULL) {
	olog() << "Sending Stop flag" << endl;
	return Traversal::Stop;
    }

    PDTNode * node = getClone(exp);
    if (node == NULL) {
	olog() << "Sending Stop flag" << endl;
	return Traversal::Stop;
    }
    PDTExpBool * expClone = dynamic_cast < PDTExpBool* > (node);
    if (expClone == NULL) {
	olog() << "Sending Stop flag" << endl;
	return Traversal::Stop;
    }

    if (preCount == 0) {
	string name = d.getName();
	PDTPostCondition * postClone = new PDTPostCondition(rcg, *expClone, name);
	name = name + "-post";
	PDTBoolVar * bool_post = new PDTBoolVar(rcg, name); 
	PDTAssign * post_assign = new PDTAssign(rcg, *bool_post, *expClone);
	if (post_assign == NULL) {
	    olog() << "Sending Stop flag" << endl;
	    return Traversal::Stop;
	}

	if (postClone == NULL) {
	    olog() << "Sending Stop flag" << endl;
	    return Traversal::Stop;
	}
	setClone(d, bool_post);

	// create the pre post relation
	if (pendingPre == NULL) {
	    olog() << "sending Stop flag" << endl;
	    return Traversal::Stop;
	}

	PDTNode * node = getClone(pendingPre);
	if (node == NULL) {
	    olog() << "sending Stop flag" << endl;
	    return Traversal::Stop;
	}

	PDTBoolVar * bool_pre = dynamic_cast <PDTBoolVar *>(node);
	if (bool_pre == NULL) {
	    olog() << "sending Stop flag" << endl;
	    return Traversal::Stop;
	}

	PDTExpBool * exp1 = dynamic_cast<PDTExpBool*>(bool_pre);
	PDTExpBool * exp2 = dynamic_cast<PDTExpBool*>(bool_post);
	PDTImplies * implies = new PDTImplies(rcg, *exp1, *exp2);
	if (implies == NULL) {
	    olog() << "sending Stop flag" << endl;
	    return Traversal::Stop;
	}

	PDTNot * not_implies = new PDTNot(rcg, *implies);
	if (not_implies == NULL) {
	    olog() << "sending Stop flag" << endl;
	    return Traversal::Stop;
	}

    // for dprove need to give it not(pre->post) noted after experimenting
	PDTAssert * full_condition = new PDTAssert(rcg, *not_implies);
	//PDTAssert * full_condition = new PDTAssert(rcg, *implies);
	if (full_condition == NULL) {
	    olog() << "sending Stop flag" << endl;
	    return Traversal::Stop;
	}

	return Traversal::Continue;
    } else {
	return Traversal::Continue;
    }
}


// PDTPreCondition 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTPreCondition & d) {
    if (getClone(d) != NULL)
	return Traversal::Skip;

    PDTExpBool * exp = d.getExpression();
    if (exp == NULL) {
	olog() << "Sending Stop flag" << endl;
	return Traversal::Stop;
    }

    PDTNode * node = getClone(exp);
    if (node == NULL) {
	olog() << "Sending Stop flag" << endl;
	return Traversal::Stop;
    }
    PDTExpBool * expClone = dynamic_cast < PDTExpBool* > (node);
    if (expClone == NULL) {
	olog() << "Sending Stop flag" << endl;
	return Traversal::Stop;
    }

    if (isFirstPre) {
	/**
	 * Create a boolean var to hold the precondition value
	 * Varname = func_name::pre_name;
	 * This function is part of the function's stack
	 */
	string name = d.getName();
	PDTPreCondition * preClone = new PDTPreCondition(rcg, *expClone, name);
	name = name + "-pre";
	PDTBoolVar * bool_pre = new PDTBoolVar(rcg, name); 
	PDTAssign * pre_assign = new PDTAssign(rcg, *bool_pre, *expClone);
	if (pre_assign == NULL) {
	    olog() << "Sending Stop flag" << endl;
	    return Traversal::Stop;
	}

	if (preClone == NULL) {
	    olog() << "Sending Stop flag" << endl;
	    return Traversal::Stop;
	}
	setClone(d, bool_pre->getNode());
	pendingPre = &d;
	return Traversal::Continue;
    } else {
	// TODO: tranform into normal condition to be held at the end in the 
	// entire function
	return Traversal::Continue;
    }
}


// PDTProp 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTProp & d) {
    NOT_IMPLEMENTED_YET
    return Traversal::Continue;
}


// PDTRelation 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTRelation & d) {
    NOT_IMPLEMENTED_YET
    return Traversal::Continue;
}


// PDTSequence 
Traversal::RetType PDTGraphCloneTraversal :: pre(PDTSequence & d) {
    if (getClone(d) != NULL)
        return Traversal::Skip;

    string _name = d.getName();
    PDTType * eType = d.getElementType(); // can be NULL

    PDTIntRange * range = d.getRange();
    PDTIntRange * rangeClone;
    if (range != NULL) {
        if (range->traverseEx(*this) == Traversal::Stop) {
            olog() << "sending signal stop!" << endl;
            return Traversal::Stop;
        }
        rangeClone = dynamic_cast<PDTIntRange*> (getClone(range));
    } else {
        rangeClone = range; // i.e. it is NULL
    }

    PDTIntRange * elRange = d.getElRange();
    PDTIntRange * elRangeClone;
    if (elRange != NULL) {
        if (elRange->traverseEx(*this) == Traversal::Stop) {
            olog() << "sending signal stop!" << endl;
            return Traversal::Stop;
        } 
        elRangeClone = dynamic_cast<PDTIntRange*> (getClone(elRange));
    } else {
        elRangeClone = elRange; // i.e. it is NULL
    }

    unsigned int size = d.getSize();
    
    PDTSequence * seq = new PDTSequence(rcg, _name, eType, rangeClone, elRangeClone, size);
    setClone(d, seq);
    
    return Traversal::Continue;
}


// PDTSequenceAccessBool 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTSequenceAccessBool & d) {
    CLONE_BINARY_OP_LR(PDTSequenceAccessBool,PDTSequenceVar,PDTExpNum)
}


// PDTSequenceAccessNum 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTSequenceAccessNum & d) {
    CLONE_BINARY_OP_LR(PDTSequenceAccessNum,PDTSequenceVar,PDTExpNum)
}


// PDTSequenceAssign 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTSequenceAssign & d) {
    NOT_IMPLEMENTED_YET
    return Traversal::Continue;
}


// PDTSequenceVar 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTSequenceVar & d) {
    PDTSequence * seq = d.getSequence();
    PDTNode * node = getClone(seq);
    PDTSequence * cloneSeq = dynamic_cast<PDTSequence*>(node);
    if (cloneSeq == NULL) {
        olog() << "sending signal stop!" << endl;
        return Traversal::Stop;
    }
    CLONE_SEQ_VAR(PDTSequenceVar, cloneSeq)
}


// PDTSet 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTSet & d) {
    NOT_IMPLEMENTED_YET
    return Traversal::Continue;
}


// PDTSetVar 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTSetVar & d) {
    NOT_IMPLEMENTED_YET
    return Traversal::Continue;
}


// PDTSubt 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTSubt & d) {
    CLONE_BINARY_OP(PDTSubt,PDTExpNum)
}

/**
 * Return true when statement is not a while and not an if else 
 * and not a list of statements, and has a quantifier child
 */
int
PDTGraphCloneTraversal :: hasQuantifier(PDTNode * stmt) {
    if (stmt->isListOfStatements() || stmt->isWhile() || stmt->isIfElse())
        return -1;

    if (stmt->isQuantifier())
        return 0;

    vector < PDTNode * > & children = stmt->getChildren();
    for (unsigned int i = 0; i < children.size(); i++) {
        PDTNode * node = children[i];
        if (node->isQuantifier())
            return i;
    }
    return -1;
}

PDTNode * PDTGraphCloneTraversal :: quantifierHandler(PDTNode * node, int childId) {
    if (node->traverseEx(*this) == Traversal::Stop)
        return NULL;

    PDTNode * clone = getClone(node);
    if (clone == NULL)
        return NULL;

    cout << "ChildId is = " << childId << endl;
    PDTNode & qNode = node->getChildEx(childId);
    PDTNode * qList = quantifierStatement[qNode.getId()]; 
    if (qList == NULL) {
        cerr << "qList is NULL" << endl;
        return NULL;
    }
    vector < PDTStatement * > stmts;
    stmts.push_back(dynamic_cast<PDTStatement*>(qList));
    stmts.push_back(dynamic_cast<PDTStatement*>(clone));
    PDTListOfStatements * list = new PDTListOfStatements(rcg, stmts);
    return list;
}

// PDTWhile 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTWhile & d) {
    PDTExpBool* cond = d.getCondition();
    PDTNode * condClone = getClone(cond);
    PDTExpBool* condExpClone = dynamic_cast<PDTExpBool*>(condClone);
    if (condExpClone == NULL)
        return Traversal::Stop;

    PDTStatement* loop = d.getLoopStatement();
    PDTNode * loopClone;
    int childid;
    if (loop->isQuantifier())
        loopClone = quantifierStatement[loop->getId()];
    else if ((childid = hasQuantifier(loop)) != -1)
        loopClone = quantifierHandler(loop, childid); 
    else
        loopClone = getClone(loop);
    PDTStatement * loopStatementClone = dynamic_cast<PDTStatement*>(loopClone);
    if (loopStatementClone == NULL)
        return Traversal::Stop;

    PDTWhile * clone = new PDTWhile(rcg, *condExpClone, *loopStatementClone);
    if (clone == NULL)
        return Traversal::Stop;
    setClone(d,clone);
    return Traversal::Continue;
}

// PDTXor 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTXor & d) {
    CLONE_BINARY_OP(PDTXor,PDTExpBool)
}


// PDTUnresolvedExp 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTUnresolvedExp & d) {
    CLONE_CONST()
}


// PDTType 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTType & d) {
    //CLONE_CONST()
    return Traversal::Continue;
}


// PDTUnaryNumExpr 
Traversal::RetType PDTGraphCloneTraversal :: post(PDTUnaryNumExpr & d) {
    PDTUnaryOp & op = d.isMinus()? 
        PDTUnaryOp::PDTUnaryMinus :
        PDTUnaryOp::PDTUnaryPlus;

    PDTNode* cClone = getChildClone(d,0); 
    PDTExpNum* expClone = dynamic_cast<PDTExpNum*>(cClone); 
    if (expClone == NULL) 
        return Traversal::Stop; 
    PDTUnaryNumExpr* clone = new PDTUnaryNumExpr(rcg, op, *expClone);
    if (clone == NULL)
        return Traversal::Stop;
    setClone(d,clone);
    return Traversal::Continue;
}
